﻿module Pattern
    type Pat = | Cmd of int        (* command identifier *)
               | Seq of Pat * Pat  (* sequence of 2 commands *)
               | Loop of int * Pat (* Loop(command idnetifier, loop body pattern) *)
               | Pow of Pat * int  (* Pow(p,i) = p^i, i.e., i repetitions of the pattern p *)
               | Skip              (* Skip command gets its own pattern since it has special
                                      handling in the pattern product *)

    let rec eq(p1 : Pat, p2 : Pat) = match (p1,p2) with
                                     | (Cmd(i1),Cmd(i2)) -> i1 = i2
                                     | (Seq(p1,p2),Seq(p1',p2')) -> eq(p1,p1') && eq(p2,p2')
                                     | (Loop(i1,p1),Loop(i2,p2)) -> i1 = i2 && eq(p1,p2)
                                     | (Pow(p1,i1),Pow(p2,i2)) -> i1 = i2 && eq(p1,p2)
                                     | (Skip,Skip) -> true
                                     | _ -> false

    let naiveProd(p1 : Pat, p2 : Pat) = match (p1,p2) with
     (* skip is ignored *)              | (Skip,_) -> p2
     (* skip is ignored *)              | (_,Skip) -> p1
     (* Remove repetitions of loop body
        after loop correction *)        | (Loop(i,p),p') -> if eq(p,p') then Loop(i,p) else Seq(p1,p2)
     (* Concat two power patterns *)    | (Pow(p1',i1),Pow(p2',i2)) -> if eq(p1',p2') then Pow(p1',i1+i2) else Seq(p1,p2)
     (* increase power by 1 *)          | (Pow(p1',i1),p2') -> if eq(p1',p2') then Pow(p1',i1+1) else Seq(p1,p2)
     (* increase power by 1 *)          | (p2',Pow(p1',i1)) -> if eq(p1',p2') then Pow(p1',i1+1) else Seq(p1,p2)
                                        | _ -> if eq(p1,p2) then Pow(p1,2) else Seq(p1,p2)

    let rec reduce(p : Pat) = match p with
                                | Loop(i,p) -> Loop(i,reduce(p))
                                | Seq(p1,p2) -> naiveProd(reduce(p1),reduce(p2))
                                | _ -> p

    let prod(p1 : Pat, p2 : Pat) =
        let p = naiveProd(p1,p2)
        let rec lfp f x = if x = f x then x else lfp f <| f x
        lfp reduce p

    let rec size(p : Pat) = 1 + match p with
                                | Seq(p1,p2) -> size(p1) + size(p2) (* sequence of 2 commands *)
                                | Loop(_,p') -> size(p') (* Loop(command idnetifier, loop body pattern) *)
                                | Pow(p',_) -> size(p')  (* Pow(p,i) = p^i, i.e., i repetitions of the pattern p *)
                                | _ -> 0

    let isSmaller(p1,p2) = size(p1) < size(p2)

    let smaller(p1,p2) = if isSmaller(p1,p2) then p1 else p2